\begin{tabbing}
@$i$: with declarations ds:${\it ds}$da:${\it da}$effect of $k$(v) is $x$ := $f$ s v($j$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if eqof(IdDeq)($j$,$i$)\+
\\[0ex]then \=with declarations \+
\\[0ex]ds:${\it ds}$
\\[0ex]da:${\it da}$
\\[0ex]effect of $k$(v) is $x$ := $f$ s v
\-\\[0ex]else 
\\[0ex]fi 
\-
\end{tabbing}